本发明属于SOA技术领域,具体为增强SOA可生存性的降级服务替换验证方法。主要步骤:1.采用进程代数形式化建模WS-BPEL描述文件所体现的组合服务交互协议,包括:服务契约,成员服务可允许的消息交互;2.流程决策点,分析流程形式服务的消息操作(即发送、接受消息)选择。采用白盒策略描述WS-BPEL流程形式的替换服务和候选服务、以及服务组合和替换的上下文环境。3.将服务替换准则确定为服务相容性被定义为组合系统的可执行完成属性。在此基础上,4.验证实施替换后不影响系统相容性的降级服务替换,以及实施替换后的降级系统是否满足用户需求。本发明解决了现有技术无法验证降级服务替换正确性的问题。
1.一种增强SOA可生存性的降级服务替换验证方法,其特征在于具体步骤为:步骤一、采用进程代数形式化建模WS-BPEL描述文件所体现的组合服务交互协议利用进程代数这一形式化工具对服务及其组合环境进行形式化建模,其中,成员服务及组合服务的系统模型表示为服务契约;所述服务契约用以描述服务外部可观测的消息行为;由于WS-BPEL提供了参与组合的服务集合、服务的调用关系和消息的往来信息,这里采用白盒策略描述WS-BPEL流程形式的替换服务和候选服务以及服务组合和替换的上下文环境;采用xa0xa0xa0xa0xa0xa0xa0xa0xa0xa0xa0xa0xa0xa0xa0xa0xa0xa0xa0xa0xa0xa0xa0xa0xa0xa0xa0xa0xa0xa0xa0xa0xa0xa0xa0xa0xa0xa0xa0xa0xa0xa0xa0xa0xa0xa0xa0xa0ntent="drawing" img-format="jpg" inline="no" orientation="portrait" wi="12"/>演算描述一个WS-BPEL流程服务即服务契约C,具体语法如下: ntent="drawing" img-format="jpg" inline="no" orientation="portrait" wi="150"/> ntent="drawing" img-format="jpg" inline="no" orientation="portrait" wi="516"/> 这里,ntent="drawing" img-format="jpg" inline="no" orientation="portrait" wi="12"/>表示流程服务的一个接口,ntent="drawing" img-format="jpg" inline="no" orientation="portrait" wi="45"/>表示发送消息操作,即沿接口ntent="drawing" img-format="jpg" inline="no" orientation="portrait" wi="12"/>发出消息ntent="drawing" img-format="jpg" inline="no" orientation="portrait" wi="18"/>;ntent="drawing" img-format="jpg" inline="no" orientation="portrait" wi="45"/>表示接收消息操作,即沿接口ntent="drawing" img-format="jpg" inline="no" orientation="portrait" wi="12"/>接收消息xa0ntent="drawing" img-format="jpg" inline="no" orientation="portrait" wi="18"/>;ntent="drawing" img-format="jpg" inline="no" orientation="portrait" wi="11"/>表示没有消息交互的内部操作;根据服务契约的操作语义规则,ntent="drawing" img-format="jpg" inline="no" orientation="portrait" wi="53"/>表示服务契约ntent="drawing" img-format="jpg" inline="no" orientation="portrait" wi="12"/>执行操作ntent="drawing" img-format="jpg" inline="no" orientation="portrait" wi="12"/>后演化为ntent="drawing" img-format="jpg" inline="no" orientation="portrait" wi="17"/>,ntent="drawing" img-format="jpg" inline="no" orientation="portrait" wi="32"/>表示隐藏操作,xa0意味着在ntent="drawing" img-format="jpg" inline="no" orientation="portrait" wi="12"/>中的消息操作xa0ntent="drawing" img-format="jpg" inline="no" orientation="portrait" wi="12"/>变为ntent="drawing" img-format="jpg" inline="no" orientation="portrait" wi="11"/>,即,当多个服务组合成一个服务系统时,某些服务可能仅提供部分接口,并且某些接口及其相关消息操作变成了内部不可观察的;步骤二、建立流程决策点,分析WS-BPEL流程形式服务的消息交互行为在WS-BPEL流程服务交互环境中,区分三类服务契约的决策点:(1)仅有发送消息操作的决策点;xa0(2)仅有接受消息操作的决策点;(3)同时包括发送消息操作和接受消息操作的决策点;其中,第三类流程决策点是指同一服务接口的发送消息操作和接受消息操作;步骤三、建立服务替换正确性准则,定义服务相容性包括两大部分:其一,是在所有计算路径上完成属性;其二,在部分计算路径上的“测试成功”;设一组WS-BPEL流程服务ntent="drawing" img-format="jpg" inline="no" orientation="portrait" wi="108"/>组合,记为系统ntent="drawing" img-format="jpg" inline="no" orientation="portrait" wi="180"/>;系统ntent="drawing" img-format="jpg" inline="no" orientation="portrait" wi="12"/>满足完成相容属性,记为ntent="drawing" img-format="jpg" inline="no" orientation="portrait" wi="29"/>,如果下列条件之一成立:(1)xa0如果ntent="drawing" img-format="jpg" inline="no" orientation="portrait" wi="12"/>是自包含系统,对于任意ntent="drawing" img-format="jpg" inline="no" orientation="portrait" wi="17"/>以致ntent="drawing" img-format="jpg" inline="no" orientation="portrait" wi="56"/>,ntent="drawing" img-format="jpg" inline="no" orientation="portrait" wi="48"/>;(2)xa0如果ntent="drawing" img-format="jpg" inline="no" orientation="portrait" wi="12"/>是开放系统,对于任意ntent="drawing" img-format="jpg" inline="no" orientation="portrait" wi="17"/>以致ntent="drawing" img-format="jpg" inline="no" orientation="portrait" wi="53"/>,存在ntent="drawing" img-format="jpg" inline="no" orientation="portrait" wi="21"/>以致ntent="drawing" img-format="jpg" inline="no" orientation="portrait" wi="51"/>;步骤四、降级服务替换正确性验证包括两部分:其一,服务子契约以较少的可交换消息集保持了所有计算路径上的服务相容性;其二,服务契约的测试精化,在部分计算路径上保持了服务相容性;一个WS-BPEL流程服务契约ntent="drawing" img-format="jpg" inline="no" orientation="portrait" wi="18"/>是另一服务契约ntent="drawing" img-format="jpg" inline="no" orientation="portrait" wi="18"/>的子契约,记为ntent="drawing" img-format="jpg" inline="no" orientation="portrait" wi="60"/>,如果下列条件成立:(1)如果ntent="drawing" img-format="jpg" inline="no" orientation="portrait" wi="18"/>是一个决策点即顶层操作是一个选择,那么ntent="drawing" img-format="jpg" inline="no" orientation="portrait" wi="18"/>也是一个和ntent="drawing" img-format="jpg" inline="no" orientation="portrait" wi="18"/>具有相同类型的决策点;(2)对于每个接收消息操作ntent="drawing" img-format="jpg" inline="no" orientation="portrait" wi="42"/>以致ntent="drawing" img-format="jpg" inline="no" orientation="portrait" wi="80"/>,存在ntent="drawing" img-format="jpg" inline="no" orientation="portrait" wi="81"/>以致ntent="drawing" img-format="jpg" inline="no" orientation="portrait" wi="72"/>;(3)对于每个发送消息操作ntent="drawing" img-format="jpg" inline="no" orientation="portrait" wi="45"/>以致ntent="drawing" img-format="jpg" inline="no" orientation="portrait" wi="81"/>,存在ntent="drawing" img-format="jpg" inline="no" orientation="portrait" wi="80"/>,以致ntent="drawing" img-format="jpg" inline="no" orientation="portrait" wi="72"/>;如果,WS-BPEL流程服务契约ntent="drawing" img-format="jpg" inline="no" orientation="portrait" wi="18"/>是ntent="drawing" img-format="jpg" inline="no" orientation="portrait" wi="18"/>的子契约,那么,对于相同的运行环境ntent="drawing" img-format="jpg" inline="no" orientation="portrait" wi="12"/>,ntent="drawing" img-format="jpg" inline="no" orientation="portrait" wi="18"/>替换ntent="drawing" img-format="jpg" inline="no" orientation="portrait" wi="18"/>后不改变系统原有的完成属性,即:如果ntent="drawing" img-format="jpg" inline="no" orientation="portrait" wi="60"/>,那么,ntent="drawing" img-format="jpg" inline="no" orientation="portrait" wi="228"/>xa0;在使用子契约实施替换后,一个系统仍保持系统原有的相容性;然而,由于使用子契约实施的替换是不等价替换,所以,系统的某些服务行为可能会受到影响,这个影响分为两方面:第一,如果子契约提供了更多的消息接收能力,并且具有相同的发送消息非决定性选择,那么,这个替换不影响系统的运行,并且系统将具有更多的服务能力;第二,如果子契约提供了更多的消息接收能力,但是发送消息的非决定性选择减少,即发送更少的消息,那么,替换会对系统的全局行为产生两个方面的影响,即:(1)xa0较少的消息交换集合;(2)较少的可完成计算路径;最后,实现增强SOA系统可生存性的降级服务替换;这里,用保留的服务契约来描述降级服务替换后用户期望保留的系统功能,记为ntent="drawing" img-format="jpg" inline="no" orientation="portrait" wi="63"/>;其中,ntent="drawing" img-format="jpg" inline="no" orientation="portrait" wi="12"/>是WS-BPEL流程服务系统;依据正确服务替换的要求,实施服务替换后必须满足xa0ntent="drawing" img-format="jpg" inline="no" orientation="portrait" wi="102"/>;令ntent="drawing" img-format="jpg" inline="no" orientation="portrait" wi="181"/>,其中,ntent="drawing" img-format="jpg" inline="no" orientation="portrait" wi="14"/>是WS-BPEL流程服务契约,且ntent="drawing" img-format="jpg" inline="no" orientation="portrait" wi="49"/>,ntent="drawing" img-format="jpg" inline="no" orientation="portrait" wi="102"/>;对于任意ntent="drawing" img-format="jpg" inline="no" orientation="portrait" wi="77"/>,xa0ntent="drawing" img-format="jpg" inline="no" orientation="portrait" wi="156"/>如果下列条件成立:(1)xa0ntent="drawing" img-format="jpg" inline="no" orientation="portrait" wi="60"/>;(2)xa0对于每个消息发送操作ntent="drawing" img-format="jpg" inline="no" orientation="portrait" wi="44"/>以致ntent="drawing" img-format="jpg" inline="no" orientation="portrait" wi="192"/>,在xa0ntent="drawing" img-format="jpg" inline="no" orientation="portrait" wi="23"/>中也存在ntent="drawing" img-format="jpg" inline="no" orientation="portrait" wi="44"/>。技术领域
本发明属于SOA技术领域,具体涉及一种SOA降级服务替换正确性验证的方法。
背景技术
任何系统都不可避免地会发生故障。面向服务的架构SOA(Servicexa0Orientedxa0Architecture)的软件(服务)系统也不例外。众所周知,以备用的候选服务替代产生故障的服务或系统,是一种性质有效的系统可用性增强方法。系统从发生故障到恢复正常工作的这个紧急修复时间内,成功实施服务替换面临的最大挑战是迅速找到可用的候选服务。作为一种特例,迅速找到与被替换服务完全等价的候选服务。实践中,对于一个关键任务(Mission-Critical)系统,在其故障修复期间内,既无法期望系统立即恢复工作(因为故障),又不容忍整个系统彻底失效(因为承担着关键任务)。所能选择的,是一个具有可生存性的系统。即,系统不必工作在正常状态,但仍然能够继续提供有限的功能的服务,尤其是提供核心服务。在这种紧急情况下,允许降级服务替换是主要应急措施之一。在这种可生存性环境中,降级服务替换面临的关键问题,是采取什么替换关系理论可保证实施替换后的系统仍可保持服务相容性。中国专利申请(申请号200710025615.X,公开号101130402)给出了一种基于行为一致的服务替换方法。该方法要求,服务提供者在注册服务时须提供服务的行为描述,即合法操作序列。服务使用者在实施替换时检查候选服务与原始被替换服务的行为一致性。在服务替换时,行为一致性通过行为观察一致性规则来验证。另一中国专利申请(申请号201110058676.2,公开号102082737A)给出了一种基于服务优先级的替换方法。该方法分析了组合服务的非功能属性,即服务质量QoS(Qualityxa0ofxa0Services),并以此定义服务优先级。专利申请201110058676.2不具备降级替换的能力和相应的验证技术。上述两项中国专利申请,分别从功能属性和非功能属性方面仅保证了等价(或升级)服务替换的正确性,而不能完成降级服务可替换性的验证。在可生存性环境中的紧急修复时间内,往往难以迅速找到与被替换服务完全等价的候选服务。此外,在愈来愈普及的云计算环境中,为了降低运维成本,服务消费者通常会主动采用降级服务。因此,研究降级服务的可替换性验证技术很有必要。
发明内容
本发明的目的在于提供一种SOA降级服务替换正确性验证的方法,以解决现有技术只能从功能属性和非功能属性方面保证等价(或升级)服务替换的正确性,而不能完成降级服务可替换性的验证问题。本发明是针对具有交互协议、流程形式服务的降级替换验证。一种典型的对象是国际工业标准WS-BPEL(Webxa0Servicesxa0–xa0Businessxa0Processxa0Executionxa0Language)组合流程服务。对于替换服务和候选服务,以及服务组合和替换的上下文环境,其服务接口、接口上的消息操作以及消息交互协议均为已知。任何软件系统都不可避免发生故障,系统从发生故障到恢复正常工作的紧急修复时间内,成功实施服务替换面临的最大挑战是迅速找到可用的候选服务。尤其是,很难迅速找到与被替换服务完全等价的候选服务。本发明针对不同结构的候选服务,验证服务替换的正确性,特别地,验证降级服务替换的正确性,并满足如下要求:确认实施替换后不影响系统相容性的降级服务替换;确认实施替换后的系统能满足用户要求。本发明提出的SOA降级服务替换正确性验证方法,其流程如附图1,具体步骤为: 步骤一、采用进程代数形式化建模WS-BPEL描述文件所体现的组合服务交互协议 国际工业标准WS-BPEL是最为广泛使用的组合服务描述方式。本发明利用进程代数这一形式化工具对服务及其组合环境进行形式化建模,如附图1中1.1所示。其中,成员服务及组合服务的系统模型表示为服务契约。服务契约用以描述服务外部可观测的消息行为;由于WS-BPEL提供了参与组合的服务集合、服务的调用关系和消息的往来信息,这里便可采用白盒策略描述WS-BPEL流程形式的替换服务和候选服务以及服务组合和替换的上下文环境(附图1中1.2)。采用xa0xa0xa0xa0xa0xa0xa0xa0xa0xa0xa0xa0xa0xa0xa0xa0xa0xa0xa0xa0xa0xa0xa0xa0xa0xa0xa0xa0xa0xa0xa0xa0xa0xa0xa0xa0xa0xa0xa0xa0xa0xa0xa0xa0xa0xa0xa0xa0ntent="drawing" img-format="jpg" inline="no" orientation="portrait" wi="13"/>演算描述一个WS-BPEL流程服务(即服务契约)C,具体语法如下: ntent="drawing" img-format="jpg" inline="no" orientation="portrait" wi="167"/> ntent="drawing" img-format="jpg" inline="no" orientation="portrait" wi="386"/> 这里,ntent="drawing" img-format="jpg" inline="no" orientation="portrait" wi="13"/>表示流程服务的一个接口。ntent="drawing" img-format="jpg" inline="no" orientation="portrait" wi="45"/>表示发送消息操作,即沿接口ntent="drawing" img-format="jpg" inline="no" orientation="portrait" wi="13"/>发出消息ntent="drawing" img-format="jpg" inline="no" orientation="portrait" wi="19"/>;ntent="drawing" img-format="jpg" inline="no" orientation="portrait" wi="45"/>表示接收消息操作,即沿接口ntent="drawing" img-format="jpg" inline="no" orientation="portrait" wi="13"/>接收消息xa0ntent="drawing" img-format="jpg" inline="no" orientation="portrait" wi="19"/>;ntent="drawing" img-format="jpg" inline="no" orientation="portrait" wi="11"/>表示没有消息交互的内部操作。服务契约的操作语义规则详见附图1。其中,ntent="drawing" img-format="jpg" inline="no" orientation="portrait" wi="53"/>表示服务契约ntent="drawing" img-format="jpg" inline="no" orientation="portrait" wi="13"/>执行操作ntent="drawing" img-format="jpg" inline="no" orientation="portrait" wi="13"/>后演化为ntent="drawing" img-format="jpg" inline="no" orientation="portrait" wi="17"/>。ntent="drawing" img-format="jpg" inline="no" orientation="portrait" wi="32"/>表示隐藏操作,xa0意味着在ntent="drawing" img-format="jpg" inline="no" orientation="portrait" wi="13"/>中的消息操作xa0ntent="drawing" img-format="jpg" inline="no" orientation="portrait" wi="13"/>变为ntent="drawing" img-format="jpg" inline="no" orientation="portrait" wi="11"/>。即,当多个服务组合成一个服务系统时,某些服务可能仅提供部分接口,并且某些接口及其相关消息操作变成了内部不可观察的。 步骤二、建立流程决策点,分析WS-BPEL流程形式服务的消息交互行为 在WS-BPEL流程服务交互环境中,区分三类服务契约的决策点:(1)仅有发送消息操作的决策点;xa0(2)仅有接受消息操作的决策点;(3)同时包括发送消息操作和接受消息操作的决策点。其中,第三类流程决策点是指同一服务接口的发送消息操作和接受消息操作。 步骤三、建立服务替换正确性准则,定义服务相容性 包括两大部分:其一,是在所有计算路径上完成属性,如附图1中3.1,其二,在部分计算路径上的“测试成功”,如附图1中3.2部分。如附图1中2所示,一组WS-BPEL流程服务ntent="drawing" img-format="jpg" inline="no" orientation="portrait" wi="108"/>组合,记为系统ntent="drawing" img-format="jpg" inline="no" orientation="portrait" wi="181"/>。系统ntent="drawing" img-format="jpg" inline="no" orientation="portrait" wi="13"/>满足完成相容属性,记为ntent="drawing" img-format="jpg" inline="no" orientation="portrait" wi="29"/>,如果下列条件之一成立:(1)xa0如果ntent="drawing" img-format="jpg" inline="no" orientation="portrait" wi="13"/>是自包含系统,对于任意ntent="drawing" img-format="jpg" inline="no" orientation="portrait" wi="17"/>以致ntent="drawing" img-format="jpg" inline="no" orientation="portrait" wi="55"/>,ntent="drawing" img-format="jpg" inline="no" orientation="portrait" wi="49"/>;(2)xa0如果ntent="drawing" img-format="jpg" inline="no" orientation="portrait" wi="13"/>是开放系统,对于任意ntent="drawing" img-format="jpg" inline="no" orientation="portrait" wi="17"/>以致ntent="drawing" img-format="jpg" inline="no" orientation="portrait" wi="53"/>,存在ntent="drawing" img-format="jpg" inline="no" orientation="portrait" wi="21"/>以致ntent="drawing" img-format="jpg" inline="no" orientation="portrait" wi="52"/>。 步骤四、降级服务替换正确性验证 包括两部分(如附图1中4):其一,服务子契约以较少的可交换消息集保持了所有计算路径上的服务相容性,如附图1中4.1;其二,服务契约的测试精化,在部分计算路径上保持了服务相容性,如附图1中4.2。一个WS-BPEL流程服务契约ntent="drawing" img-format="jpg" inline="no" orientation="portrait" wi="19"/>是另一服务契约ntent="drawing" img-format="jpg" inline="no" orientation="portrait" wi="19"/>的子契约,记为ntent="drawing" img-format="jpg" inline="no" orientation="portrait" wi="60"/>,如果下列条件成立:(1)如果ntent="drawing" img-format="jpg" inline="no" orientation="portrait" wi="19"/>是一个决策点(即顶层操作是一个选择),那么ntent="drawing" img-format="jpg" inline="no" orientation="portrait" wi="19"/>也是一个和ntent="drawing" img-format="jpg" inline="no" orientation="portrait" wi="19"/>具有相同类型的决策点;(2)对于每个接收消息操作ntent="drawing" img-format="jpg" inline="no" orientation="portrait" wi="43"/>以致ntent="drawing" img-format="jpg" inline="no" orientation="portrait" wi="80"/>,存在ntent="drawing" img-format="jpg" inline="no" orientation="portrait" wi="81"/>以致ntent="drawing" img-format="jpg" inline="no" orientation="portrait" wi="72"/>;(3)对于每个发送消息操作ntent="drawing" img-format="jpg" inline="no" orientation="portrait" wi="45"/>以致ntent="drawing" img-format="jpg" inline="no" orientation="portrait" wi="81"/>,存在ntent="drawing" img-format="jpg" inline="no" orientation="portrait" wi="80"/>,以致ntent="drawing" img-format="jpg" inline="no" orientation="portrait" wi="72"/>。在上述条件中,条件(1)要求二者具有相同类型的决策点;条件(2)要求子契约不能提供更少的接收消息的能力;条件(3)要求子契约不能有更少的发送消息决定性选择。递归条件描述了在交互协议中对操作次序的要求。如果,WS-BPEL流程服务契约ntent="drawing" img-format="jpg" inline="no" orientation="portrait" wi="19"/>是ntent="drawing" img-format="jpg" inline="no" orientation="portrait" wi="19"/>的子契约,那么,对于相同的运行环境ntent="drawing" img-format="jpg" inline="no" orientation="portrait" wi="13"/>,ntent="drawing" img-format="jpg" inline="no" orientation="portrait" wi="19"/>替换ntent="drawing" img-format="jpg" inline="no" orientation="portrait" wi="19"/>后不改变系统原有的完成属性,即:如果ntent="drawing" img-format="jpg" inline="no" orientation="portrait" wi="60"/>,那么,ntent="drawing" img-format="jpg" inline="no" orientation="portrait" wi="229"/>。在使用子契约实施替换后,一个系统仍可保持系统原有的相容性。然而,由于使用子契约实施的替换是不等价替换,所以,系统的某些服务行为可能会受到影响。这个影响分为两方面:第一,如果子契约提供了更多的消息接收能力,并且具有相同的发送消息非决定性选择,那么,这个替换不影响系统的运行,并且系统将具有更多的服务能力。第二,如果子契约提供了更多的消息接收能力,但是发送消息的非决定性选择减少,即发送更少的消息,那么,替换会对系统的全局行为产生两个方面的影响,即:(1)xa0较少的消息交换集合;(2)较少的可完成计算路径。最后,实现了增强SOA系统可生存性的降级服务替换,如附图1中5。这里,用保留的服务契约来描述降级服务替换后用户期望保留的系统功能,记为ntent="drawing" img-format="jpg" inline="no" orientation="portrait" wi="64"/>。其中,ntent="drawing" img-format="jpg" inline="no" orientation="portrait" wi="13"/>是WS-BPEL流程服务系统。依据正确服务替换的要求,实施服务替换后必须满足xa0ntent="drawing" img-format="jpg" inline="no" orientation="portrait" wi="100"/>。令ntent="drawing" img-format="jpg" inline="no" orientation="portrait" wi="180"/>。其中,ntent="drawing" img-format="jpg" inline="no" orientation="portrait" wi="15"/>是WS-BPEL流程服务契约,且ntent="drawing" img-format="jpg" inline="no" orientation="portrait" wi="49"/>,ntent="drawing" img-format="jpg" inline="no" orientation="portrait" wi="101"/>。对于任意ntent="drawing" img-format="jpg" inline="no" orientation="portrait" wi="76"/>,xa0ntent="drawing" img-format="jpg" inline="no" orientation="portrait" wi="156"/>如果下列条件成立:(1)xa0ntent="drawing" img-format="jpg" inline="no" orientation="portrait" wi="61"/>;(2)xa0对于每个消息发送操作ntent="drawing" img-format="jpg" inline="no" orientation="portrait" wi="45"/>以致ntent="drawing" img-format="jpg" inline="no" orientation="portrait" wi="192"/>,在xa0ntent="drawing" img-format="jpg" inline="no" orientation="portrait" wi="23"/>中也存在ntent="drawing" img-format="jpg" inline="no" orientation="portrait" wi="45"/>。本发明采用进程代数对已注册的流程服务进行行为建模(即服务契约),而不要求服务提供者在注册服务时必须提供服务的行为描述。对于替换关系,本发明的技术采用偏序关系(即子服务契约),而不是等价关系理论(如行为一致性等)。因此可获得专利申请200710025615.X所不具备的降级服务替换能力。本发明的核心内容,即流程服务降级替换验证技术,在功能属性分析方面突破了既有的等价(或升级)服务替换技术。本发明采用进程代数将具有交互协议的、流程形式的服务进行形式化建模;采用白盒策略,通过描述交互服务允许的接收/发送消息序列,刻画服务的消息交互行为。通过描述服务系统的契约,刻画成员服务间可允许的交互行为。服务替换准则即服务相容性被定义为组合系统的执行可完成属性。在此基础上,可验证实施替换后不影响系统相容性的降级服务替换,以及实施替换后的系统是否满足用户要求。
附图说明
图1为增强SOA系统可生存性的降级服务替换验证流程。图2为服务契约操作语义规则。图3为组合服务应用系统Travel。图4具有不同的内部结构的两个WS-BPEL服务。图5为降级形式的Travel服务。
具体实施方式
以下以旅行组合服务应用Travel为例,说明本发明的具体实施例。如附图3所示,一个简化的xa0Travelxa0应用,包括四个成员服务:xa0Travel、Hotel、Airline和Bank。Travel接受并响应来自客户的请求,Hotelxa0和xa0Airlinexa0分别提供酒店和航班的预定服务,Bankxa0为其他服务提供公共的支付服务。在服务组合应用xa0Travelxa0中,每个角色都可由来自不同服务提供商的不同版本的具体WS-BPEL服务来实现。成员服务xa0Travelxa0也是如此。在正常情况下,Travelxa0的相关服务由具体服务xa0Trvl1xa0来实现。现在,由于某些系统故障,Trvl1xa0失效。于是,寻找xa0Travelxa0的另一具体实现Trvl2是保持整个流程得以继续执行的一种有效的办法。具体WS-BPEL服务Trvl1和Trvl2具有不同的内部结构,如附图4所示。现验证采用ntent="drawing" img-format="jpg" inline="no" orientation="portrait" wi="47"/>替换ntent="drawing" img-format="jpg" inline="no" orientation="portrait" wi="47"/>后Travel系统的正确性,具体过程如下:1、采用进程代数对两个WS-BPEL服务进行形式化建模,得到如下服务契约:xa0ntent="drawing" img-format="jpg" inline="no" orientation="portrait" wi="453"/>; ntent="drawing" img-format="jpg" inline="no" orientation="portrait" wi="497"/>;其中,ntent="drawing" img-format="jpg" inline="no" orientation="portrait" wi="383"/>。2、采用流程决策点分析ntent="drawing" img-format="jpg" inline="no" orientation="portrait" wi="47"/>与ntent="drawing" img-format="jpg" inline="no" orientation="portrait" wi="47"/>。两个WS-BPEL流程均包括三个流程决策点,即航班预订ntent="drawing" img-format="jpg" inline="no" orientation="portrait" wi="35"/>、酒店预订ntent="drawing" img-format="jpg" inline="no" orientation="portrait" wi="35"/>以及支付ntent="drawing" img-format="jpg" inline="no" orientation="portrait" wi="31"/>。关于航班预订,ntent="drawing" img-format="jpg" inline="no" orientation="portrait" wi="47"/>与ntent="drawing" img-format="jpg" inline="no" orientation="portrait" wi="47"/>具有相同的决策点,即相同的接受和发送消息;关于决策点“酒店预订”,ntent="drawing" img-format="jpg" inline="no" orientation="portrait" wi="47"/>比ntent="drawing" img-format="jpg" inline="no" orientation="portrait" wi="47"/>具有更少的发送消息操作;关于决策点“支付”,ntent="drawing" img-format="jpg" inline="no" orientation="portrait" wi="47"/>比ntent="drawing" img-format="jpg" inline="no" orientation="portrait" wi="47"/>具有更多的接受消息操作。3、服务替换的正确性准则为服务相容性,即ntent="drawing" img-format="jpg" inline="no" orientation="portrait" wi="201"/>。4、验证ntent="drawing" img-format="jpg" inline="no" orientation="portrait" wi="47"/>替换ntent="drawing" img-format="jpg" inline="no" orientation="portrait" wi="47"/>后Travel系统的正确性。依据流程服务子契约,ntent="drawing" img-format="jpg" inline="no" orientation="portrait" wi="116"/>。因此,采用ntent="drawing" img-format="jpg" inline="no" orientation="portrait" wi="47"/>替换ntent="drawing" img-format="jpg" inline="no" orientation="portrait" wi="47"/>后的Travel系统将仍然保持相容性,即ntent="drawing" img-format="jpg" inline="no" orientation="portrait" wi="201"/>。然而,由于ntent="drawing" img-format="jpg" inline="no" orientation="portrait" wi="47"/>比ntent="drawing" img-format="jpg" inline="no" orientation="portrait" wi="47"/>具有更少的发送消息操作,采用ntent="drawing" img-format="jpg" inline="no" orientation="portrait" wi="47"/>替换ntent="drawing" img-format="jpg" inline="no" orientation="portrait" wi="47"/>后的Travel系统将以降级的形式提供服务,如附图5所示。采用ntent="drawing" img-format="jpg" inline="no" orientation="portrait" wi="47"/>替换ntent="drawing" img-format="jpg" inline="no" orientation="portrait" wi="47"/>后的Travel系统,仅只能提供预订酒店Htl1的服务,而不能再提供预订酒店Htl2的服务。最后,还需验证采用ntent="drawing" img-format="jpg" inline="no" orientation="portrait" wi="47"/>替换ntent="drawing" img-format="jpg" inline="no" orientation="portrait" wi="47"/>后的Travel系统是否满足用户需求。如果用户要求必需保留预订酒店Htl1的服务,那么,可以采用ntent="drawing" img-format="jpg" inline="no" orientation="portrait" wi="47"/>替换ntent="drawing" img-format="jpg" inline="no" orientation="portrait" wi="47"/>,即ntent="drawing" img-format="jpg" inline="no" orientation="portrait" wi="253"/>。如果用户要求必需保留预订酒店Htl2的服务,那么,采用ntent="drawing" img-format="jpg" inline="no" orientation="portrait" wi="47"/>替换ntent="drawing" img-format="jpg" inline="no" orientation="portrait" wi="47"/>是不正确的。考虑另一个WS-BPEL实现: ntent="drawing" img-format="jpg" inline="no" orientation="portrait" wi="416"/>。此时,ntent="drawing" img-format="jpg" inline="no" orientation="portrait" wi="253"/>。通过考察服务组合应用xa0Trave中采用ntent="drawing" img-format="jpg" inline="no" orientation="portrait" wi="47"/>替换ntent="drawing" img-format="jpg" inline="no" orientation="portrait" wi="47"/>的正确性,说明了本发明在具体实施过程是可行的。本发明的另一种实施例是用于降低云计算中软件(服务)的运维成本的主动降级服务替换的正确性验证。在云计算中,云服务商提供云服务,用户为使用的服务进行按需支付。为此,提供商主动提供多种等级化的服务选择,并辅以更为经济的付费模式和价格。云用户可以选择自我需要的降级服务,替换业务流程或工作流中原有成员服务。从而达到节省成本的目的。在云计算实施例中,实施方式是形式化描述WS-BPEL服务与验证满足用户需求的降级服务替换正确性。在主动降级时,用户更多考虑在要求的部分路上的相容性。在验证满足用户需求的降级服务替换正确性时,仍须依据组件4.1的服务子契约关系保证系统在所有路径上的相容性,或者依据组件4.2的“测试成功”保持用户要求的部分路上的相容性。xa0